doc: before-requesting-review checklist (AGENTS.md + ErdosProblems README)#4378
Open
williamjblair wants to merge 4 commits into
Open
doc: before-requesting-review checklist (AGENTS.md + ErdosProblems README)#4378williamjblair wants to merge 4 commits into
williamjblair wants to merge 4 commits into
Conversation
|
👋 This is an automated welcome message. 🤖 A few friendly reminders while the review gets started:
Thanks again for helping improve Formal Conjectures. |
williamjblair
changed the title
williamjblair
changed the title
3 tasks
mo271
reviewed
Jul 5, 2026
mo271
left a comment
mo271
left a comment
Collaborator
There was a problem hiding this comment.
Thanks!
Added a few suggestion for improvement.
Comment on lines
+64
to
+68
| 3. **Search before defining.** Check `FormalConjecturesForMathlib` and | ||
| neighboring problem files for existing definitions, API, and notation | ||
| before introducing your own. If something you need seems generally useful, | ||
| it belongs in `FormalConjecturesForMathlib`, not inlined in the problem | ||
| file. |
Collaborator
There was a problem hiding this comment.
This sould go to AGENTS.md: it is not ErdosProblems specific
Comment on lines
+69
to
+71
| 4. **Keep commentary out of the Lean file.** Notes to reviewers, formalization | ||
| choices, and caveats belong in the pull request description, not the | ||
| source. |
Comment on lines
+72
to
+73
| 5. **Use LaTeX, not backticks, for mathematics in docstrings.** See | ||
| `AGENTS.md` for the exceptions on the Lean-API side. |
Collaborator
There was a problem hiding this comment.
Probably not worth repeating here?
Comment on lines
+74
to
+75
| 6. **Add sanity tests for new definitions.** A nontrivial definition should | ||
| come with at least one `@[category test]` statement exercising it. |
| - [ ] Docstrings present for main definitions | ||
| - [ ] `research open`, `textbook` and `research solved` docstrings include a concise description | ||
| - [ ] Code properly formatted and readable | ||
| - [ ] Searched `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding new ones |
Collaborator
There was a problem hiding this comment.
Suggested change
| - [ ] Searched `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding new ones | |
| - [ ] Searched mathlib and `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding new ones |
| - [ ] `research open`, `textbook` and `research solved` docstrings include a concise description | ||
| - [ ] Code properly formatted and readable | ||
| - [ ] Searched `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding new ones | ||
| - [ ] Notes to reviewers (formalization choices, caveats) are in the PR description, not the Lean file |
Collaborator
There was a problem hiding this comment.
Suggested change
| - [ ] Notes to reviewers (formalization choices, caveats) are in the PR description, not the Lean file | |
| - [ ] Notes to reviewers (formalization choices, caveats, AI support used) are in the PR description, not the Lean file |
| - Add large proofs (this is a benchmark repository, not a proof repository) | ||
| - Use camelCase for theorem names | ||
| - Create placeholder definitions in FormalConjecturesForMathlib/ | ||
| - Redefine notation or API that already exists in `FormalConjecturesForMathlib` or a neighboring problem file |
Collaborator
There was a problem hiding this comment.
Suggested change
| - Redefine notation or API that already exists in `FormalConjecturesForMathlib` or a neighboring problem file | |
| - Redefine notation or API that already exists in mathlib, `FormalConjecturesForMathlib` or a neighboring problem file |
mo271
reviewed
Jul 5, 2026
Comment on lines
+69
to
+70
| 4. **Keep commentary out of the Lean file.** Notes to reviewers, formalization | ||
| choices, and caveats belong in the pull request description, not the |
Collaborator
There was a problem hiding this comment.
some formalisation choices are probably good to keep in the docstrings/comments
…specific items in the README - AGENTS.md: search mathlib too, add 'AI support used', include mathlib in the redefine-notation pitfall (mo271's suggestions) - ErdosProblems/README: drop the general checklist items (search-before-defining, commentary-out-of-Lean, LaTeX-not-backticks, sanity-tests); they live in AGENTS.md. Keep the two erdosproblems.com-specific ones and link the general checklist.
Contributor
Author
|
Thanks! Applied all three AGENTS.md suggestions, and moved the general items out of the ErdosProblems README (they're covered by the Quality Checklist) so only the erdosproblems.com-specific ones remain. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Puts the recurring review corrections into the two files authors and their agents already read:
AGENTS.md: two rules that come up in review but weren't written anywhere: searchFormalConjecturesForMathliband neighboring files before defining anything (ErdosProblems: add 199, 224, 226, 246, 296, 363 (#3998 sync) #4343, ErdosProblems: add 31, 34, 47, 280 (#3998 sync) #4345), and keep notes-to-reviewers in the PR description rather than the Lean file (feat(ErdosProblems): add 755 #4036). Added to the existing Quality Checklist and DON'T list.FormalConjectures/ErdosProblems/README.md: a "Before requesting review" section with the Erdős-specific items (verbatim docstrings and solution attributions, ErdosProblems: formalise 11 solved problems, linking plby/lean-proofs #4319), following the pattern of the naming and docstring conventions already in that file.Every line traces to a real review comment on a merged PR. Doc-only; follows up on the Zulip discussion about making the repetitive half of review a checklist authors and their agents tick off.
cc @mo271